Inference at * 2 
Iof proof for Lemma zero ann a:



1. a : 
2. b : 
3. b = 0
  (a * b) = 0 

latex

 by (% This should be automatic! % 
((HypSubst 3 0) 
(CollapseTHEN ((Auto_aux (first_nat 1:n
(C) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t) inil_term)))) 

latex

(C.

Definitions

, t  T